Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(c(c(a, y, a), b(x, z), a)) → b(y, f(c(f(a), z, z)))
f(b(b(x, f(y)), z)) → c(z, x, f(b(b(f(a), y), y)))
c(b(a, a), b(y, z), x) → b(a, b(z, z))
Q is empty.
We use [23] with the following order to prove termination.
Lexicographic path order with status [19].
Quasi-Precedence:
[f1, c3] > b2 > a
Status: a: multiset
c3: [2,3,1]
b2: [2,1]
f1: [1]